header {
  package com.googlecode.kipler.parsing;
  import com.googlecode.kipler.*;
  import com.googlecode.kipler.satisfiability.*;
  import com.googlecode.kipler.satisfiability.container.*;
  import com.googlecode.kipler.syntax.*;
  import com.googlecode.kipler.syntax.formula.*;
  import com.googlecode.kipler.syntax.concept.*;
  import java.util.*;
}  

class FormulaParser extends Parser;

options {
        buildAST=true;
	k = 5;
}

world:			(namespaceArea)? semiColSeparatedFormula { #world = #([WORLD], #world); } ;
semiColSeparatedFormula:formula (SEMICOLON^ formula)* SEMICOLON! ;
namespaceArea:		namespace (SEMICOLON^ namespace)* SEMICOLON! ;
namespace:		NAMESPACE^ LPAREN! PREFIX COLON! NCName RPAREN! ;

// well formed formulas
formulaWithNs:		namespaceArea formula ;
formula:		(LPAREN! formula1)=> LPAREN! formula1 RPAREN! ((UNTIL^ | BEFORE^) LPAREN! formula1 RPAREN!)+ 
			| formula1
			;
formula1:		((NEXT^ | SOMETIME^ | GENERALLY^) LPAREN! formula)=> unaryLTLFormula
			| dlFormula 
			| booleanFormula 
			| negFormula;
negFormula:		NOT^ LPAREN! formula RPAREN! ;
dlFormula:              (role IMPLIES_ROLE)=> roleInclusion
                        | (role LPAREN uriReference COMMA)=> objectRoleAssertion
			| (concept (EQUALS | IMPLIES))=> conceptDefinition 
			| roleAssertion
                        | conceptAssertion
                        | sameIndividualAssertion;
roleInclusion:          role IMPLIES_ROLE^ role ;
roleAssertion:          TRANSITIVE^ LPAREN! role RPAREN! ;
conceptAssertion:	concept LPAREN! uriReference  RPAREN! { #conceptAssertion = #([CONCEPT_ASSERTION], #conceptAssertion); } ;
objectRoleAssertion:	role LPAREN! uriReference COMMA! uriReference RPAREN! { #objectRoleAssertion = #([OBJECT_ROLE_ASSERTION], #objectRoleAssertion); } ;
conceptDefinition:	concept (EQUALS^ | IMPLIES^) concept ;
sameIndividualAssertion:uriReference DOUBLE_EQUAL^ uriReference;
booleanFormula:		(AND^ | OR^) LPAREN! formula COMMA! commaSeparatedFormula RPAREN! ;
commaSeparatedFormula:	formula (COMMA^ formula)* ;
unaryLTLFormula:	(NEXT^ | SOMETIME^ | GENERALLY^) LPAREN! formula RPAREN! ;

// well formed concepts
concept:		concept1 ((BAR^ | UNTIL^ | BEFORE^) concept1)* 
			;
concept1: 		concept2 (AMP^ concept2)* ;
concept2:		(TILDE^)? (atomicConcept 
                        | generalizedConcept 
                        | roleQuantification 
                        | qualifiedNoRestriction 
                        | nominal
			| unaryLTLConcept) ;
atomicConcept:		uriReference ;
generalizedConcept:	LPAREN! concept RPAREN! ;
roleQuantification:	(SOME^ | ALL^) LPAREN! role COMMA! concept RPAREN! ;
qualifiedNoRestriction: (GREATER_THAN_OR_EQ^ | LESS_THAN_OR_EQ^) LPAREN! unsignedInt COMMA! role COMMA! concept RPAREN! ;
nominal:                LBRACE^ uriReference RBRACE! ;
unaryLTLConcept:	(NEXT^ | SOMETIME^ | GENERALLY^) LPAREN! concept RPAREN! ;

// general elements
role:			uriReference | DASH^ LPAREN! uriReference RPAREN! ;
term:			uriReference | VARIABLE ;
uriReference:		NCName | QNAME ;
unsignedInt:		UNSIGNED_INT ;

class FormulaLexer extends Lexer;

options {
    k=2; // needed for newline junk
    charVocabulary='\u0000'..'\ufffe'; // allow unicode
}

tokens {
   NOT        = "not" ;
   AND        = "and" ;
   OR         = "or" ;
   SOME       = "some" ;
   ALL        = "all" ;
   TRANSITIVE = "transitive" ;
   NAMESPACE  = "ns" ;
   NEXT	      = "X" ;
   SOMETIME   = "F" ;
   GENERALLY  = "G" ;
   UNTIL      = "U" ;
   BEFORE     = "B" ;
}

// The following are used to form artificial ASTs
protected WORLD                 : "world" ;
protected CONCEPT_ASSERTION     : "ca" ;
protected OBJECT_ROLE_ASSERTION : "ora" ;

LPAREN            :   '(' ;
RPAREN            :   ')' ;
VARIABLE          :   QUESTION (ALPHANUMERIC)+ ;
LESS_THAN_OR_EQ   :   LESS_THAN EQUALS ;
GREATER_THAN_OR_EQ:   GREATER_THAN EQUALS ;
EQUALS            :   '=' ;
AMP               :   '&' ;
BAR               :   '|' ;
CARET             :   '^' ;
COLON             :   ':' ;
COMMA             :   ',' ;
IMPLIES           :   DASH GREATER_THAN ;
IMPLIES_ROLE      :   GREATER_THAN DASH ;
DOUBLE_EQUAL      :   EQUALS EQUALS ; 
UNSIGNED_INT      :   (DIGIT)+ ;
SEMICOLON         :   ';' ;
STRING_LITERAL    :   '\"'! (CHAR_ESC | ~('\"'|'\\') )* '\"'! ; // ~('\\') )* (options {greedy=true;}:WS)? '\"'! ;
TILDE             :   '~' ;
UNDERSCORE        :   '_' ;
LBRACE            :   '{' ;
RBRACE            :   '}' ;
DASH              :   '-' ;

// escape sequence inside a string literal
protected
CHAR_ESC:
    '\\'
    ( 'n'  { $setText("\n"); }
    | 'r'  { $setText("\r"); }
    | 't'  { $setText("\t"); }
    | 'b'  { $setText("\b"); }
    | 'f'  { $setText("\f"); }
    | '\"' { $setText("\""); }
    | '\'' { $setText("\'"); }
    | '\\' { $setText("\\"); }
    )
;

PREFIX_LOCALNAME_OR_QNAME
	:	(PREFIX COLON LOCAL_NAME)=>	PREFIX COLON LOCAL_NAME		{ $setType(QNAME) ; }
	|	(PREFIX)=>			PREFIX				{ $setType(PREFIX) ; }
	|	(LOCAL_NAME)=>	    		LOCAL_NAME			{ $setType(LOCAL_NAME) ; } 
	;

protected PREFIX:		(LETTER)+ ;
protected LOCAL_NAME: 		LETTER (LETTER | DIGIT | UNDERSCORE | POINT | DASH)* ;

protected NCBegin : (LOWER_CASE_LETTER | UNDERSCORE | UPPER_CASE_LETTER);
protected NCRest: (NCBegin | POINT | DASH | HASH | SLASH | AMP | QUESTION | DIGIT | COLON | TILDE);

NCName: LESS_THAN! NCBegin (NCRest)* GREATER_THAN!;

protected GREATER_THAN: '>';
protected LESS_THAN: 	'<';
protected HASH: '#';
protected SLASH: '/';
protected QUESTION: '?';
protected LOWER_CASE_LETTER: 'a'..'z';
protected UPPER_CASE_LETTER: 'A'..'Z';
protected LETTER: (LOWER_CASE_LETTER | UPPER_CASE_LETTER);
protected DIGIT: '0'..'9';
protected ALPHANUMERIC: (LETTER | DIGIT);
protected POINT: '.' ;
protected LBRACKET:	'[';
protected RBRACKET:	']';

WS    : ( ' '
        | '\r' '\n'
        | '\n'
        | '\t'
        )
        {$setType(Token.SKIP);}
      ;


class FormulaTreeParser extends TreeParser;

options {
	importVocab=FormulaParser;
}

{
   private Set<Formula> formulaSet = new LinkedHashSet<Formula>();
}


world returns [Set<Formula> result = null]
	:	( #(WORLD namespaceArea) ) => #(WORLD namespaceArea semiColSeparatedFormula)
		{
		 result = formulaSet;
		}
	| 	#(WORLD semiColSeparatedFormula)
		{
		 result = formulaSet;
		}
	;

semiColSeparatedFormula
{ Formula a, b; }
	: 	( #(SEMICOLON formula formula) ) => #(SEMICOLON a=formula b=formula)
		{
		 formulaSet.add(a);
		 formulaSet.add(b);
		}
	|	#(SEMICOLON semiColSeparatedFormula b=formula)
		{
		 formulaSet.add(b);
		}
	|	(a=formula) 
		{
		 formulaSet.add(a);
		}
	;
	
namespaceArea
	:	( #(SEMICOLON namespace namespace) ) => #(SEMICOLON namespace namespace)
	|	#(SEMICOLON namespaceArea namespace)
	|	namespace
	;

namespace
	:	#(NAMESPACE p:PREFIX uri:NCName)
		{
		 NameManager.getInstance().addPrefix(p.getText(), uri.getText());
		}
	;

formulaWithNs returns [Formula result = null]
	:	(namespaceArea result=formula)
	;
	
formula returns [Formula result = null]
{ Formula a, b; }
	:	(result=booleanFormula)
	|	(result=dlFormula)
	| 	(result=ltlFormula)
	|	#(NOT a=formula)
		{
		 result = a.toggleNegated();
		}
	;


booleanFormula returns [Formula result = null]
{ Formula a, b; }
	:	#(COMMA a=formula b=formula)
		{
		 BooleanFormula bf = new BooleanFormula(BooleanFormula.Operator.OR, a, b);
		 result = bf;
		}
	|	#(AND a=formula b=formula)
		{
		 BooleanFormula bf = new BooleanFormula(BooleanFormula.Operator.AND, a, b);
		 ParserUtility.assignAndOperatorToBinarySubformulae(bf);
		 result = bf;
		}
	|	#(OR a=formula b=formula)
		{
		 BooleanFormula bf = new BooleanFormula(BooleanFormula.Operator.OR, a, b);
		 result = bf;
		}
	;

ltlFormula returns [Formula result = null]
{ Formula a, b; }
	:	#(NEXT a=formula)
		{
		 result = new LTLUnaryFormula(LTLUnaryOperator.NEXT, a);
		}
	|	#(GENERALLY a=formula)
		{
		 result = new LTLUnaryFormula(LTLUnaryOperator.ALWAYS, a);
		}
	|	#(SOMETIME a=formula)
		{
		 result = new LTLUnaryFormula(LTLUnaryOperator.SOMETIME, a);
		}
	|	#(UNTIL a=formula b=formula)
		{
		 result = new LTLBinaryFormula(LTLBinaryOperator.UNTIL, a, b);
		}
	|	#(BEFORE a=formula b=formula)
		{
		 result = new LTLBinaryFormula(LTLBinaryOperator.BEFORE, a, b);
		}
	;

dlFormula returns [Formula f = null]
{ String t, u, conceptName; 
  Concept d, e;
  Role role1, role2; }
	:	#(OBJECT_ROLE_ASSERTION role1=role t=term u=term) // #(NCName term literal) ) => #(role:NCName t=term u=literal)
		{
		 ObjectRoleAssertion ra = new ObjectRoleAssertion(role1, t, u);
		 f = ra;
		}
	|	#(CONCEPT_ASSERTION d=concept t=uriReference)  
    		{
		 ConceptAssertion ca = new ConceptAssertion(d, t); 
		 f = ca;
		}		
	|	#(EQUALS d=concept e=concept)
		{
		 ConceptDefinition cd = new ConceptDefinition(ConceptDefinition.Type.NON_PRIMITIVE, d, e);
		 f = cd;
		}
	|	#(IMPLIES d=concept e=concept)
		{
		 ConceptDefinition cd = new ConceptDefinition(ConceptDefinition.Type.PRIMITIVE, d, e);
		 f = cd;
		}
        |       #(IMPLIES_ROLE role1=role role2=role)
                {
                 RoleInclusion ri = new RoleInclusion(role1, role2);
                 f = ri;
                }
        |       #(TRANSITIVE role1=role)
                {
                 RoleAssertion ra = new RoleAssertion(RoleAssertion.Type.TRANSITIVE, role1);
                 f = ra;
                }
        |       #(DOUBLE_EQUAL t=uriReference u=uriReference)
                {
                 SameIndividualAssertion sia = new SameIndividualAssertion(t, u);
                 f = sia;
                }
	;

concept returns [Concept result = null]
{ Concept cd1, cd2;
  Role roleName;
  String conceptName;
  int no; }
	:	#(TILDE cd1=concept)
		{
		 result = cd1.toggleNegated();
		}
	|	#(AMP cd1=concept cd2=concept)
		{
		 BooleanConcept bd = new BooleanConcept(BooleanConcept.Constructor.INTERSECTION, cd1, cd2);
		 result = bd;
		}
	|	#(BAR cd1=concept cd2=concept)
		{
		 BooleanConcept bd = new BooleanConcept(BooleanConcept.Constructor.UNION, cd1, cd2);
		 result = bd;
		}
	|	#(ALL roleName=role cd1=concept)
		{
		 RoleQuantification vr = new RoleQuantification(RoleQuantification.Constructor.ALL, roleName, cd1);
		 result = vr;
		}
	|	#(SOME roleName=role cd1=concept)
		{
		 RoleQuantification vr = new RoleQuantification(RoleQuantification.Constructor.SOME, roleName, cd1);
		 result = vr;
		}
	|	#(LESS_THAN_OR_EQ no=unsignedInt roleName=role cd1=concept)
		{
		 QualifiedNoRestriction qr = new QualifiedNoRestriction(InequalityConstructor.AT_MOST, no, roleName, cd1);
		 result = qr;
		}
	|	#(GREATER_THAN_OR_EQ no=unsignedInt roleName=role cd1=concept)
		{
		 QualifiedNoRestriction qr = new QualifiedNoRestriction(InequalityConstructor.AT_LEAST, no, roleName, cd1);
		 result = qr;
		}
        |       #(LBRACE conceptName=uriReference)
		{
		 Nominal nominal = new Nominal(conceptName);
		 result = nominal;
		}
	|	#(NEXT cd1=concept)
		{
		 result = new LTLUnaryConcept(LTLUnaryOperator.NEXT, cd1);
		}
	|	#(GENERALLY cd1=concept)
		{
		 result = new LTLUnaryConcept(LTLUnaryOperator.ALWAYS, cd1);
		}
	|	#(SOMETIME cd1=concept)
		{
		 result = new LTLUnaryConcept(LTLUnaryOperator.SOMETIME, cd1);
		}
	|	#(UNTIL cd1=concept cd2=concept)
		{
		 result = new LTLBinaryConcept(LTLBinaryOperator.UNTIL, cd1, cd2);
		}
	|	#(BEFORE cd1=concept cd2=concept)
		{
		 result = new LTLBinaryConcept(LTLBinaryOperator.BEFORE, cd1, cd2);
		}
	| 	conceptName=uriReference 
		{ 
		 ConceptName c = new ConceptName();
		 c.setName(conceptName);
		 result = c; 
		}
	;

role returns [Role role = null] 
{ String roleName; }
	:	#(DASH roleName=uriReference)
		{
		 role = new Role(roleName, true);
		}	
	|	roleName=uriReference
		{
		 role = new Role(roleName);
		}
	;

term returns [String term = null]
	:	term=uriReference
	|	var:VARIABLE {term = var.getText();}
	;
	
uriReference returns [String absoluteUri = null] 
	:	qname:QNAME 
		{
		 String qStr = qname.getText();
		 int colonIndex = qStr.indexOf(':');
		 String prefix = qStr.substring(0, colonIndex);
		 String label = qStr.substring(colonIndex + 1);
		 String namespace = NameManager.getInstance().getURI(prefix); // TODO: if null, throw exception
		 absoluteUri = namespace + label;
		}	
	|	uri:NCName { absoluteUri = uri.getText(); }
	;
	

unsignedInt returns [int n = 0]
	:	theNo:UNSIGNED_INT { n = Integer.parseInt(theNo.getText()); }
	;
